first-order logic

Definition (first-order logic)

Let $\mathcal{V} = \{x,y,...,\}$ be a set of variables.
Let $\mathcal{R} = \{P,Q,...\}$ and $\mathcal{F} = \{f,g,...\}$ be a vocabulary of predicate/function symbols.
predicate and function symbols equipped with arity $\operatorname{ar} : \mathcal{R} \cup \mathcal{F} \to \mathbb{N}$
first-order terms and formulas over 𝒱,ℛ,ℱ\mathcal{V}, \mathcal{R}, \mathcal{F} given by grammar:
- $s, t ::= x \mid f(t_1,...,t_{\operatorname{ar}(f)})$ (terms)
- ϕ,ψ::=⊤|⊥\phi, \psi ::= \top \mid \bot (atomic truth values)
  - $\mid P(t_1,...,t_{\operatorname{ar}(f)}) \mid s = t$ (predicates and equality)
  - $\mid \phi \lor \psi \mid \neg \phi$ (Boolean connectives)
  - $\mid \exists x.\phi$ (existential quantification)
further connectives definable:
- $\phi \to \psi \triangleq \neg \phi \lor \psi$
- $s \neq t \triangleq \neg (s=t)$
- $\phi \land \psi \triangleq \neg(\neg \phi \lor \neg \psi)$
- $\forall x.\phi \triangleq \neg(\exists x.\neg\phi)$
- etc.
fix precedence to avoid parentheses: $\neg$ > $\land, \lor$ > $\exists, \forall$

first-order logic allows general assertions using quantifiers
- universal quantifier $\forall$
- existential quantifier ∃\exists
  - it is dual to universal quantifier (c.f. modal logic $\Box$ and $\Diamond$ )